w:World, e:E. first(e)  (t:. t<time(e)  isnull(a(loc(e);t))) 

latex

Definitions	False, t  T, P  Q, a<b, n-m, <a,b>, E, {x:A| B(x) }, , b, x:AB(x), Id, , x:AB(x), x:A. B(x), S  T, w-pred(w;e), Unit, Type, isl(x), b, Prop, A, , s = t, #$n, AB, -n, n+m, Void, a(i;t), isnull(a), P & Q, P  Q, left+right, inl(x), if b t else f fi, false, i=j, , inr(x), True, first(e), World, x.A(x), time(e), ij, P  Q, Dec(P), {T}, SQType(T), s ~ t
Lemmas	nat sq, w-pred-wf2, decidable lt, ge wf, nat properties, w-time wf, nat wf, first wf, world wf, true wf, it wf, not functionality wrt iff, assert of eq int, eq int wf, ifthenelse wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, w-isnull wf, w-a wf, le wf, bool wf, not wf, assert wf, bnot wf, isl wf, w-E wf, unit wf, w-pred wf, false wf